Inference at * 
Iof proof for Lemma nil fseg:


  T:Type, l:(T List). fseg(T;[];l) 

latex

 by ((((Unfold `fseg` 0) 
CollapseTHEN (Auto'))) 
CollapseTHEN (((InstConcl [l]) 

CoCollapseTHEN (Auto)))) 

latex

C1: 

C1: 1. T : Type
C1: 2. l : T List
C1:   l = (l @ [])
C.

Definitions	fseg(T;L1;L2), x:A. B(x), x:A  B(x), Type, , as @ bs, x:A. B(x), x:AB(x), s = t, t  T, [], type List
Lemmas	append wf